$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$, $b$:($T$ List).
\\[0ex]l\_disjoint($T$;$a$;l\_intersection(${\it eq}$;$a$;$b$)) $\Rightarrow$ l\_disjoint($T$;$a$;$b$)